[Merged by Bors] - feat: improve polyrith by testing for membership in the radical
#7790
Conversation
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
|
Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause |
|
The code is above what I actually feel that I understand, but is this testing membership in the radical or whether some explicit power of the element lies in the ideal? More explicitly, could it not be the case that a larger power than what is being used would work? As I said, I do not really understand the code, so I hope that this question is not just noise! |
|
It tests for membership in the radical. To start, the goal is In Sage: introduce a new variable Take So the Grobner basis computation produces I'm not sure that this procedure makes any claim about finding a minimal |
|
Robert, thank you for the explanation! I had missed that there was a first Gröbner basis computation and then you used the degrees of the elements of that basis to get the bound on In terms of improving feasibility, it may be good to have an option to ask Sage to check if the given element is a member of the ideal itself or whether it is contained in the radical: I expect these two computations to perform differently (where testing for membership in the ideal is likely often faster) and you may be satisfied with the answer to one of the two questions. I am thinking of something in the style of
Anyway, this is just a suggestion: I am very happy that |
|
I thought about the two versions, but decided against it for a few reasons:
|
|
Rob, thanks for the further comments! I agree that specifying term orders normally has a much larger impact on feasibility of a Gröbner basis computation! Thanks for taking the time to explain: it turns out that my comments were indeed noise, but I am grateful for the explanations, since they taught me something! |
| [{", ".join(var_list)}] = P.gens() | ||
| p = P({goal_type}) | ||
| gens = {eq_list} + [1 - p*aux] | ||
| I = P.ideal(gens) | ||
| coeffs = P(1).lift(I) | ||
| power = max(cf.degree(aux) for cf in coeffs) | ||
| coeffs = [P(cf.subs(aux = 1/p)*p^power) for cf in coeffs[:int(-1)]] | ||
| print(str(power)+';'+serialize_polynomials(coeffs)) |
There was a problem hiding this comment.
I don't really understand why this is done with this trick of checking if 1 is in the ideal <hyps, 1/goal>, I would expect singular/sage has a way to ask for a lift to the radical ideal directly which I would hope would be easier to maintain in the long run (especially if we have aspirations of making this work for non-char 0 rings properly). Did you consider this approach?
I'm not completely against merging this, but the whole thing is starting to look a bit scary ;)
There was a problem hiding this comment.
After experimenting a bit I believe that using the builtin radical support, while probably a better algorithm underneath, is not very convenient to use with the way things are set up here, so I'm happy with this I guess
There was a problem hiding this comment.
Yeah, I remember looking for this when I first implemented this (granted, a year and a half ago) and not turning up anything useful. Sage/Singular will check for membership in the radical just fine but extracting the power and coefficient is a pain. My impression is that what I do in this PR is a "standard" approach and that a native Sage implementation would do roughly the same, although I'm somewhat out of my element here.
There was a problem hiding this comment.
When I read the sage docstring for radical earlier it said:
From the Singular manual: A combination of the algorithms
of Krick/Logar and Kemper is used. Works also in positive
characteristic (Kempers algorithm).
but I have no idea how accurate that is!
There was a problem hiding this comment.
Right -- but there's space between the membership check radical makes the former easy, but I don't see how to get from there to the latter. Maybe there's a way, I'd love to hear it.
(It sounds like you came to a similar conclusion, just leaving this comment for reference later!)
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by alexjbest. |
github-merge-queue
bot
removed this pull request from the merge queue due to no response for status checks
|
bors merge |
github-actions
bot
added
ready-to-merge
) In @hrmacbeth 's tutorial on `polyrith`, there were examples of problems that it could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a power of the goal was. ```lean example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 := sorry ``` Mathematically, `x+y*z` is in the radical of the ideal generated by `x-y, x*y`. There's a "standard trick" for testing membership in the radical without a search for the proper exponent: see e.g. section 2.2 of [arxiv.org/pdf/1007.3615.pdf](https://arxiv.org/pdf/1007.3615.pdf) or 4.2 Prop 8 of Cox, Little, O'Shea. This PR implements the trick in the Sage call made by `polyrith`. When the power returned is `n > 1`, we use `linear_combination (exp := n)` to check the certificate (#7789 ). The `polyrith` test infrastructure still needs to be ported from mathlib3. All tests in the test file succeed when they are uncommented. A future PR will restore the old test suite. Co-authored-by: Rob Lewis <[email protected]> Co-authored-by: Mario Carneiro <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
polyrith by testing for membership in the radicalpolyrith by testing for membership in the radical
) In @hrmacbeth 's tutorial on `polyrith`, there were examples of problems that it could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a power of the goal was. ```lean example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 := sorry ``` Mathematically, `x+y*z` is in the radical of the ideal generated by `x-y, x*y`. There's a "standard trick" for testing membership in the radical without a search for the proper exponent: see e.g. section 2.2 of [arxiv.org/pdf/1007.3615.pdf](https://arxiv.org/pdf/1007.3615.pdf) or 4.2 Prop 8 of Cox, Little, O'Shea. This PR implements the trick in the Sage call made by `polyrith`. When the power returned is `n > 1`, we use `linear_combination (exp := n)` to check the certificate (#7789 ). The `polyrith` test infrastructure still needs to be ported from mathlib3. All tests in the test file succeed when they are uncommented. A future PR will restore the old test suite. Co-authored-by: Rob Lewis <[email protected]> Co-authored-by: Mario Carneiro <[email protected]>
The `polyrith` feature that checks for membership in the radical of the ideal fails if the target is 0. (That is, `polyrith` cannot prove `x - x = 0`.) This PR fixes this by checking (in Sage) whether the target is 0, and short circuiting if it is. This example succeeded before #7790, fails after, and now succeeds again. ```lean import Mathlib.Tactic.Polyrith variable {R : Type*} [CommRing R] example {x : R} (H : x = 1) : x = x := by polyrith ``` This PR also renames a misleadingly named variable in the `polyrith` Python script. Co-authored-by: Rob Lewis <[email protected]>
The `polyrith` feature that checks for membership in the radical of the ideal fails if the target is 0. (That is, `polyrith` cannot prove `x - x = 0`.) This PR fixes this by checking (in Sage) whether the target is 0, and short circuiting if it is. This example succeeded before #7790, fails after, and now succeeds again. ```lean import Mathlib.Tactic.Polyrith variable {R : Type*} [CommRing R] example {x : R} (H : x = 1) : x = x := by polyrith ``` This PR also renames a misleadingly named variable in the `polyrith` Python script. Co-authored-by: Rob Lewis <[email protected]>
The `polyrith` feature that checks for membership in the radical of the ideal fails if the target is 0. (That is, `polyrith` cannot prove `x - x = 0`.) This PR fixes this by checking (in Sage) whether the target is 0, and short circuiting if it is. This example succeeded before #7790, fails after, and now succeeds again. ```lean import Mathlib.Tactic.Polyrith variable {R : Type*} [CommRing R] example {x : R} (H : x = 1) : x = x := by polyrith ``` This PR also renames a misleadingly named variable in the `polyrith` Python script. Co-authored-by: Rob Lewis <[email protected]>
The `polyrith` feature that checks for membership in the radical of the ideal fails if the target is 0. (That is, `polyrith` cannot prove `x - x = 0`.) This PR fixes this by checking (in Sage) whether the target is 0, and short circuiting if it is. This example succeeded before #7790, fails after, and now succeeds again. ```lean import Mathlib.Tactic.Polyrith variable {R : Type*} [CommRing R] example {x : R} (H : x = 1) : x = x := by polyrith ``` This PR also renames a misleadingly named variable in the `polyrith` Python script. Co-authored-by: Rob Lewis <[email protected]>
In @hrmacbeth 's tutorial on
polyrith, there were examples of problems that it could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a power of the goal was.Mathematically,
x+y*zis in the radical of the ideal generated byx-y, x*y. There's a "standard trick" for testing membership in the radical without a search for the proper exponent: see e.g. section 2.2 of arxiv.org/pdf/1007.3615.pdf or 4.2 Prop 8 of Cox, Little, O'Shea.This PR implements the trick in the Sage call made by
polyrith. When the power returned isn > 1, we uselinear_combination (exp := n)to check the certificate (#7789 ).The
polyrithtest infrastructure still needs to be ported from mathlib3. All tests in the test file succeed when they are uncommented. A future PR will restore the old test suite.